(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 2))
(let ((e4 1))
(let ((e5 5))
(let ((e6 (* v1 v0)))
(let ((e7 (- v0 v1)))
(let ((e8 (* v1 v1)))
(let ((e9 (- v1)))
(let ((e10 (- v2 e9)))
(let ((e11 (* v1 v2)))
(let ((e12 (- e9 e8)))
(let ((e13 (- e10)))
(let ((e14 (- e12 e6)))
(let ((e15 (+ e12 e6)))
(let ((e16 (* e10 e8)))
(let ((e17 (- e13 e12)))
(let ((e18 (- e10 e17)))
(let ((e19 (/ e3 (- e4))))
(let ((e20 (* e9 v0)))
(let ((e21 (+ v0 e13)))
(let ((e22 (/ e5 e5)))
(let ((e23 (>= e10 e21)))
(let ((e24 (< e14 e15)))
(let ((e25 (= e15 e8)))
(let ((e26 (>= e19 e11)))
(let ((e27 (> e7 e6)))
(let ((e28 (< e7 e19)))
(let ((e29 (= e11 e10)))
(let ((e30 (< e6 e13)))
(let ((e31 (< e8 v2)))
(let ((e32 (distinct e18 e18)))
(let ((e33 (= e11 e22)))
(let ((e34 (distinct e15 e18)))
(let ((e35 (> v0 e10)))
(let ((e36 (>= e22 e6)))
(let ((e37 (= e15 e10)))
(let ((e38 (< e20 e20)))
(let ((e39 (distinct e18 e10)))
(let ((e40 (< e8 e18)))
(let ((e41 (distinct e9 e17)))
(let ((e42 (>= e14 e10)))
(let ((e43 (< e21 e15)))
(let ((e44 (>= v1 e9)))
(let ((e45 (< e12 e14)))
(let ((e46 (= e16 e9)))
(let ((e47 (> e11 e22)))
(let ((e48 (<= v2 e20)))
(let ((e49 (<= e10 e16)))
(let ((e50 (<= e12 e14)))
(let ((e51 (= e11 e20)))
(let ((e52 (distinct e18 e18)))
(let ((e53 (>= e15 e15)))
(let ((e54 (> e15 e22)))
(let ((e55 (> e22 v1)))
(let ((e56 (>= e22 e6)))
(let ((e57 (> v1 e21)))
(let ((e58 (< e16 e14)))
(let ((e59 (= e7 v0)))
(let ((e60 (distinct v1 e10)))
(let ((e61 (>= v0 e9)))
(let ((e62 (> e13 v1)))
(let ((e63 (distinct e19 e6)))
(let ((e64 (> e16 v1)))
(let ((e65 (= e21 e14)))
(let ((e66 (> e18 v0)))
(let ((e67 (>= v0 e9)))
(let ((e68 (distinct e17 e11)))
(let ((e69 (>= e6 e9)))
(let ((e70 (= e19 e15)))
(let ((e71 (<= e12 v2)))
(let ((e72 (< e19 e19)))
(let ((e73 (<= e14 e16)))
(let ((e74 (distinct e9 v2)))
(let ((e75 (<= e21 e16)))
(let ((e76 (< e13 e18)))
(let ((e77 (< e13 e18)))
(let ((e78 (> e13 v0)))
(let ((e79 (distinct v2 e21)))
(let ((e80 (> e13 e18)))
(let ((e81 (distinct v2 e11)))
(let ((e82 (= e22 v0)))
(let ((e83 (< e16 e14)))
(let ((e84 (= v2 e8)))
(let ((e85 (and e78 e59)))
(let ((e86 (and e69 e28)))
(let ((e87 (= e81 e86)))
(let ((e88 (or e71 e75)))
(let ((e89 (not e53)))
(let ((e90 (= e88 e37)))
(let ((e91 (or e90 e60)))
(let ((e92 (xor e54 e56)))
(let ((e93 (and e91 e62)))
(let ((e94 (or e65 e52)))
(let ((e95 (xor e32 e85)))
(let ((e96 (ite e45 e40 e46)))
(let ((e97 (= e95 e84)))
(let ((e98 (=> e93 e93)))
(let ((e99 (= e80 e66)))
(let ((e100 (not e70)))
(let ((e101 (ite e61 e33 e73)))
(let ((e102 (not e30)))
(let ((e103 (not e23)))
(let ((e104 (ite e26 e51 e34)))
(let ((e105 (xor e94 e58)))
(let ((e106 (ite e72 e98 e44)))
(let ((e107 (or e92 e100)))
(let ((e108 (and e39 e97)))
(let ((e109 (=> e104 e42)))
(let ((e110 (ite e107 e41 e82)))
(let ((e111 (not e79)))
(let ((e112 (and e74 e83)))
(let ((e113 (=> e103 e35)))
(let ((e114 (or e105 e68)))
(let ((e115 (xor e114 e89)))
(let ((e116 (=> e99 e43)))
(let ((e117 (and e38 e25)))
(let ((e118 (not e96)))
(let ((e119 (or e24 e76)))
(let ((e120 (ite e48 e57 e116)))
(let ((e121 (not e108)))
(let ((e122 (not e50)))
(let ((e123 (= e67 e31)))
(let ((e124 (=> e123 e49)))
(let ((e125 (xor e63 e102)))
(let ((e126 (ite e29 e111 e110)))
(let ((e127 (ite e36 e122 e121)))
(let ((e128 (and e119 e27)))
(let ((e129 (and e124 e109)))
(let ((e130 (ite e125 e127 e128)))
(let ((e131 (or e112 e106)))
(let ((e132 (= e113 e64)))
(let ((e133 (= e130 e120)))
(let ((e134 (=> e47 e129)))
(let ((e135 (or e117 e131)))
(let ((e136 (=> e87 e115)))
(let ((e137 (not e136)))
(let ((e138 (and e126 e77)))
(let ((e139 (= e134 e133)))
(let ((e140 (or e101 e55)))
(let ((e141 (or e139 e137)))
(let ((e142 (xor e141 e138)))
(let ((e143 (ite e140 e142 e118)))
(let ((e144 (and e132 e132)))
(let ((e145 (= e135 e135)))
(let ((e146 (ite e145 e145 e143)))
(let ((e147 (or e146 e146)))
(let ((e148 (not e147)))
(let ((e149 (and e148 e148)))
(let ((e150 (not e149)))
(let ((e151 (and e144 e150)))
e151
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
